$\forall$$T$:Type, $L_{1}$, $L_{2}$:($T$ List), $a$, $b$, $c$:$T$.
\\[0ex]no\_repeats($T$;$L_{2}$)
\\[0ex]$\Rightarrow$ $L_{1}$ $\subseteq$ $L_{2}$
\\[0ex]$\Rightarrow$ adjacent($T$;$L_{1}$;$b$;$a$)
\\[0ex]$\Rightarrow$ adjacent($T$;$L_{2}$;$c$;$a$)
\\[0ex]$\Rightarrow$ ($b$ before $c$ $\in$ $L_{2}$ $\vee$ ($b$ = $c$))